\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{holindex}[2010/28/04]

\usepackage{hyperref} % Required
\usepackage{alltt} % Required
\usepackage{ifthen} % Required

% Copy of the xnewcommand.sty definitions
% Josselin Noirel http://www.jnoirel.fr/
\def \@star@or@long #1{%
  \@ifstar {\let \l@ngrel@x = \relax #1}%
           {\@testopt {\@@star@or@long {#1}}{\long}}%
}
\@ifdefinable \@@star@or@long
  {\def \@@star@or@long #1[#2]{\def \l@ngrel@x {#2}#1}}


% define foreach
\def\foreach#1#2#3{\@firsttest@foreach{#1}{#2}#3,\@end@token}
\def\@swallow#1{}
\def\@firsttest@foreach#1#2{\@ifnextchar\@end@token{\@swallow}{\@foreach{#1}{#2}}}
\def\@test@foreach#1#2{\@ifnextchar\@end@token{\@swallow}{#2\@foreach{#1}{#2}}}
\def\@foreach#1#2#3,#4\@end@token{#1{#3}\@test@foreach{#1}{#2}#4\@end@token}


%The general stuff that should not be modified without a good reason
\newcounter{holThmCounter}
\newcounter{holTermCounter}
\newcounter{holTypeCounter}
\newboolean{holShortIndexFlag}
\newboolean{holLongIndexFlag}

\newboolean{holIndexLongTermFlag}
\newboolean{holIndexLongTypeFlag}
\newboolean{holIndexLongThmFlag}
\setboolean{holIndexLongTermFlag}{true}
\setboolean{holIndexLongTypeFlag}{true}
\setboolean{holIndexLongThmFlag}{false}

\newboolean{holThmCiteDebug}
\setboolean{holThmCiteDebug}{false}

\newcommand{\initHOLindex}{\newwrite\holaux\immediate\openout\holaux\jobname.hix\@input@{\jobname.tde}}

\newcommand{\writehixfile}[1]{\write\holaux{#1}}

\newcommand{\hollookup}[1]{\@ifundefined{HOL@#1}{??}{\@nameuse{HOL@#1}}}

\newcommand{\holdef}[2]{\@namedef{HOL@#1}{#2}}

\newcommand{\defineHOLIndex}[1]{\holdef{index}{#1}}
\newcommand{\printHOLGeneralIndex}{
\setcounter{holThmCounter}{0}
\setcounter{holTermCounter}{0}
\setcounter{holTypeCounter}{0}
{\raggedbottom
 \@input@{\jobname.tid}}}

\newcommand{\printHOLIndex}{
\setboolean{holShortIndexFlag}{false}
\setboolean{holLongIndexFlag}{false}
\printHOLGeneralIndex}

\newcommand{\printShortHOLIndex}{
\setboolean{holShortIndexFlag}{true}
\setboolean{holLongIndexFlag}{false}
\printHOLGeneralIndex}

\newcommand{\printLongHOLIndex}{
\setboolean{holShortIndexFlag}{false}
\setboolean{holLongIndexFlag}{true}
\printHOLGeneralIndex}


\newcommand{\useHOLfile}[1]{%
   \writehixfile{UseFile #1}%
}
\newcommand{\setHOLoverrides}[1]{%
   \writehixfile{Overrides #1}%
}

\newcommand{\addHOLuse}[2] {%
   \writehixfile{Printed #1 #2 \thepage}%
}


\newcommand[\protect\long]{\defineHOLthm}[2]{\holdef{thm@#1}{#2}}
\newcommand[\protect]{\useHOLthm}[1]{\addHOLuse{Thm}{#1}\hollookup{thm@#1}}
\newcommand[\protect]{\inlineHOLthm}[1]{\HOLinline{\useHOLthm{#1}}}
\newcommand[\protect]{\blockHOLthm}[1]{\begin{HOLblock}\useHOLthm{#1}\end{HOLblock}}

\newcommand[\protect\long]{\defineHOLtm}[2]{\holdef{term@#1}{#2}}
\newcommand[\protect]{\useHOLtm}[1]{\addHOLuse{Term}{#1}\hollookup{term@#1}}
\newcommand[\protect]{\inlineHOLtm}[1]{\HOLinline{\useHOLtm{#1}}}
\newcommand[\protect]{\blockHOLtm}[1]{\begin{HOLblock}\useHOLtm{#1}\end{HOLblock}}

\newcommand[\protect\long]{\defineHOLty}[2]{\holdef{type@#1}{#2}}
\newcommand[\protect]{\useHOLty}[1]{\addHOLuse{Type}{#1}:\hollookup{type@#1}}
\newcommand[\protect]{\inlineHOLty}[1]{\HOLinline{\useHOLty{#1}}}
\newcommand[\protect]{\blockHOLty}[1]{\begin{HOLblock}\useHOLty{#1}\end{HOLblock}}


% Arg 1 : Type
% Arg 2 : unique ID
% Arg 3 : label
% Arg 4 : the definition
\def\addHOLdefinition#1#2#3#4{\writehixfile{%
Definition #1 #2 {#3} {#4}
}}


\newcommand[\protect]{\defHOLty}[3]{\addHOLdefinition{Type}{#1}{#2}{#3}}
\newcommand[\protect]{\defHOLtm}[3]{\addHOLdefinition{Term}{#1}{#2}{#3}}
\newcommand[\protect]{\defHOLthm}[3]{\addHOLdefinition{Thm}{#1}{#2}{#3}}


\newcommand{\setHOLlinewidth}[1]{\writehixfile{%
   Linewidth #1
}}
\newcommand{\sortHOLIndexOccurence}{\writehixfile{%
   UseOccurenceSort
}}


% Arg 1 : Type
% Arg 2 : unique ID
% Arg 2 : options
\def\formatHOLdefinition#1#2#3{\writehixfile{%
   FormatOptions #1 #2 {#3}
}}

\def\formatHOLty#1#2{\formatHOLdefinition{Type}{#1}{#2}}
\def\formatHOLtm#1#2{\formatHOLdefinition{Term}{#1}{#2}}
\def\formatHOLthm#1#2{\formatHOLdefinition{Thm}{#1}{#2}}

\def\commentHOLdefinition#1#2#3{\writehixfile{%
   Comment #1 #2 {#3}
}}

\def\commentHOLty#1#2{\commentHOLdefinition{Type}{#1}{#2}}
\def\commentHOLtm#1#2{\commentHOLdefinition{Term}{#1}{#2}}
\def\commentHOLthm#1#2{\commentHOLdefinition{Thm}{#1}{#2}}

% Arg 1 : unique ID
% Arg 2 : label
% Arg 3 : options
% Arg 4 : the definition
\newcommand[\protect]{\formatDefHOLty}[4]{
   \defHOLty{#1}{#2}{#4}
   \formatHOLty{#1}{#3}
}
\newcommand[\protect]{\formatDefHOLtm}[4]{
   \defHOLtm{#1}{#2}{#4}
   \formatHOLtm{#1}{#3}
}

% Arg 1 : Type
% Arg 2 : unique ID
\def\indexHOLdefinition#1#2{\writehixfile{%
   ForceIndex #1 #2
}}

\def\indexHOLty#1{\indexHOLdefinition{Type}{#1}}
\def\indexHOLtm#1{\indexHOLdefinition{Term}{#1}}
\def\indexHOLthm#1{\indexHOLdefinition{Thm}{#1}}

\def\fullIndexHOLdefinition#1#2#3{\writehixfile{%
   FullIndex #1 #2 #3
}}

\def\longIndexHOLty#1{\fullIndexHOLdefinition{Type}{#1}{true}}
\def\longIndexHOLtm#1{\fullIndexHOLdefinition{Term}{#1}{true}}
\def\longIndexHOLthm#1{\fullIndexHOLdefinition{Thm}{#1}{true}}
\def\shortIndexHOLty#1{\fullIndexHOLdefinition{Type}{#1}{false}}
\def\shortIndexHOLtm#1{\fullIndexHOLdefinition{Term}{#1}{false}}
\def\shortIndexHOLthm#1{\fullIndexHOLdefinition{Thm}{#1}{false}}


\newcommand{\addHOLcite}[2]{\writehixfile{Reference #1 #2 \thepage}%
\ifthenelse{\boolean{holThmCiteDebug}}{{\tiny\texttt{#2}}\ }{}}
\newcommand[\protect]{\citePureHOLthm}[1]{\addHOLcite{Thm}{#1}\ref{hol:thm:#1}}
\newcommand[\protect]{\citePureHOLtm}[1]{\addHOLcite{Term}{#1}\ref{hol:tm:#1}}
\newcommand[\protect]{\citePureHOLty}[1]{\addHOLcite{Type}{#1}\ref{hol:ty:#1}}


\newcommand[\protect]{\citeHiddenHOLthm}[1]{\addHOLcite{Thm}{#1}}
\newcommand[\protect]{\citeHiddenHOLtm}[1]{\addHOLcite{Term}{#1}}
\newcommand[\protect]{\citeHiddenHOLty}[1]{\addHOLcite{Type}{#1}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% formating option that can easily be redefined according to personal taste
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newenvironment{HOLTermIndex}{\section*{HOL-Term Index}}{}
\newenvironment{HOLTypeIndex}{\section*{HOL-Type Index}}{}
\newenvironment{HOLThmIndex}{\section*{HOL-Theorem Index}}{}

\newcommand{\HOLThmIndexTheory}[1]{\subsection*{#1Theory}}
\newcommand{\HOLThmName}[1]{{\tt{}#1}}


% Arg 1 : number in the index
% Arg 2 : unique ID
% Arg 3 : Label
% Arg 4 : Pages
% Arg 5 : Long index?
% Arg 6 : is the pages argument non-empty?
% Arg 7 : comment
% Arg 8 : latex printed version of theorem/type/term
\newcommand{\HOLIndexEntryFormat}[8]{% 
   \makebox[0.1\textwidth][r]{(#1)\ }%number
   \begin{minipage}[t]{0.9\textwidth}%everything else in minibox
      \begin{flushright}#3 \ldots$\!$\dotfill #4\end{flushright}{%first line
      \ifthenelse{\(\not\boolean{holShortIndexFlag}\) \and %use short or
                  \(\boolean{#5} \or \boolean{holLongIndexFlag}\)}% long version
          {#7\begin{HOLblock}#8\end{HOLblock}\medskip}%long version
          {}% else short version
     }%end if-then-else
   \end{minipage}\\}


% Arg 1 : unique ID 
% Arg 2 : Label
% Arg 3 : Pages
% Arg 4 : Long index?
% Arg 5 : is the pages argument non-empty?
% Arg 6 : comment
% Arg 7 : latex printed version of theorem/type/term
\newcommand{\HOLThmIndexEntryFormat}[7]{%
   \HOLIndexEntryFormat{\arabic{holThmCounter}}{thm@#1}{#2}{#3}{#4}{#5}{#6}{#7}%
}
\newcommand{\HOLTypeIndexEntryFormat}[7]{%
   \HOLIndexEntryFormat{\arabic{holTypeCounter}}{type@#1}{#2}{#3}{#4}{#5}{#6}{#7}%
}
\newcommand{\HOLTermIndexEntryFormat}[7]{%
   \HOLIndexEntryFormat{\arabic{holTermCounter}}{term@#1}{#2}{#3}{#4}{#5}{#6}{#7}%
}


\newcommand[\protect\long]{\HOLThmIndexEntry}[7]{%
   \refstepcounter{holThmCounter}{\ifthenelse{\boolean{#5}}{\label{hol:thm:#1}}{}}%
   \HOLThmIndexEntryFormat{#1}{#2}{#3}{#4}{#5}{#6}{#7}%
}

\newcommand[\protect\long]{\HOLTypeIndexEntry}[7]{%
   \refstepcounter{holTypeCounter}{\ifthenelse{\boolean{#5}}{\label{hol:ty:#1}}{}}%
   \HOLTypeIndexEntryFormat{#1}{#2}{#3}{#4}{#5}{#6}{#7}%
}

\newcommand[\protect\long]{\HOLTermIndexEntry}[7]{%
   \refstepcounter{holTermCounter}{\ifthenelse{\boolean{#5}}{\label{hol:tm:#1}}{}}%
   \HOLTermIndexEntryFormat{#1}{#2}{#3}{#4}{#5}{#6}{#7}%
}

\newcommand[\protect]{\citeHOLthm}[1]{(HOL-Thm~\citePureHOLthm{#1})}
\newcommand[\protect]{\citeHOLtm}[1]{(HOL-Term~\citePureHOLtm{#1})}
\newcommand[\protect]{\citeHOLty}[1]{(HOL-Type~\citePureHOLty{#1})}


\newcommand[\protect]{\citePureHOLthmPrefix}[2]{\citePureHOLthm{#1#2}}
\newcommand[\protect]{\mciteHOLthmPrefix}[2]{(HOL-Thms~\foreach{\citePureHOLthmPrefix{#1}}{, }{#2})}
\newcommand[\protect]{\mciteHOLthm}[1]{\mciteHOLthmPrefix{}{#1}}
\newcommand[\protect]{\mciteHOLtm}[1]{(HOL-Terms~\foreach{\citePureHOLtm}{, }{#1})}
\newcommand[\protect]{\mciteHOLty}[1]{(HOL-Types~\foreach{\citePureHOLty}{, }{#1})}

\newcommand{\UnderscoreCommands}{%   (\cite already done)
   \do\ref \do\label
   \do\citeHOLty \do\citeHOLtm \do\citeHOLthm
   \do\mciteHOLty \do\mciteHOLtm \do\mciteHOLthm \do\mciteHOLthmPrefix
   \do\citePureHOLty \do\citePureHOLtm \do\citePureHOLthm
   \do\defineHOLty \do\defineHOLtm \do\defineHOLthm
   \do\inlineHOLty \do\inlineHOLtm \do\inlineHOLthm
   \do\blockHOLty \do\blockHOLtm \do\blockHOLthm
   \do\useHOLty \do\useHOLtm \do\useHOLthm
   \do\HOLTypeIndexEntry
   \do\HOLTermIndexEntry
   \do\HOLThmIndexEntry
}
\usepackage[strings]{underscore}
\usepackage{holtexbasic}

\initHOLindex

